/-
Copyright (c) 2024 Jireh Loreaux. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jireh Loreaux
-/
import Mathlib.Topology.Algebra.Monoid

/-! # Approximate units

An *approximate unit* is a filter `l` such that multiplication on the left (or right) by `m : α`
tends to `𝓝 m` along the filter, and additionally `l ≠ ⊥`.

Examples of approximate units include:

- The trivial approximate unit `pure 1` in a normed ring.
- `𝓝 1` or `𝓝[≠] 1` in a normed ring (note that the latter is disjoint from `pure 1`).
- In a C⋆-algebra, the filter generated by the sections `fun a ↦ {x | a ≤ x} ∩ closedBall 0 1`,
  where `a` ranges over the positive elements of norm strictly less than 1.
-/

open Filter Topology

/-- An *approximate unit* is a proper filter (i.e., `≠ ⊥`) such that multiplication on the left
(and separately on the right) by `m : α` tends to `𝓝 m` along the filter. -/
structure Filter.IsApproximateUnit {α : Type*} [TopologicalSpace α] [Mul α]
    (l : Filter α) : Prop where
  /-- Multiplication on the left by `m` tends to `𝓝 m` along the filter. -/
  tendsto_mul_left m : Tendsto (m * ·) l (𝓝 m)
  /-- Multiplication on the right by `m` tends to `𝓝 m` along the filter. -/
  tendsto_mul_right m : Tendsto (· * m) l (𝓝 m)
  /-- The filter is not `⊥`. -/
  protected [neBot : NeBot l]

namespace Filter.IsApproximateUnit

section TopologicalMonoid

variable {α : Type*} [TopologicalSpace α] [MulOneClass α]

variable (α) in
/-- A unital magma with a topology and bornology has the trivial approximate unit `pure 1`. -/
lemma pure_one : IsApproximateUnit (pure (1 : α))  where
  tendsto_mul_left m := by simpa using tendsto_pure_nhds (m * ·) (1 : α)
  tendsto_mul_right m := by simpa using tendsto_pure_nhds (· * m) (1 : α)

/-- If `l` is an approximate unit and `⊥ < l' ≤ l`, then `l'` is also an approximate unit. -/
lemma mono {l l' : Filter α} (hl : l.IsApproximateUnit) (hle : l' ≤ l) [hl' : l'.NeBot] :
    l'.IsApproximateUnit where
  tendsto_mul_left m := hl.tendsto_mul_left m |>.mono_left hle
  tendsto_mul_right m := hl.tendsto_mul_right m |>.mono_left hle

variable (α) in
/-- In a topological unital magma, `𝓝 1` is an approximate unit. -/
lemma nhds_one [ContinuousMul α] : IsApproximateUnit (𝓝 (1 : α)) where
  tendsto_mul_left m := by simpa using tendsto_id (x := 𝓝 1) |>.const_mul m
  tendsto_mul_right m := by simpa using tendsto_id (x := 𝓝 1) |>.mul_const m

/-- In a topological unital magma, `𝓝 1` is the largest approximate unit. -/
lemma iff_neBot_and_le_nhds_one [ContinuousMul α] {l : Filter α} :
    IsApproximateUnit l ↔ l.NeBot ∧ l ≤ 𝓝 1 :=
  ⟨fun hl ↦ ⟨hl.neBot, by simpa using hl.tendsto_mul_left 1⟩,
    And.elim fun _ hl ↦ nhds_one α |>.mono hl⟩

/-- In a topological unital magma, `𝓝 1` is the largest approximate unit. -/
lemma iff_le_nhds_one [ContinuousMul α] {l : Filter α} [l.NeBot] :
    IsApproximateUnit l ↔ l ≤ 𝓝 1 := by
  simpa [iff_neBot_and_le_nhds_one] using fun _ ↦ ‹_›


end TopologicalMonoid

end Filter.IsApproximateUnit
